PRISM
=====
Version: 4.5.dev
Date: Sun Mar 15 01:09:38 UTC 2020
Hostname: e72bdd194fc5
Memory limits: cudd=4g, java(heap)=11g
Command line: prism -javamaxmem 11g -cuddmaxmem 4g -ii -heuristic speed -e 1e-6 -ddextraactionvars 100 -maxiters 1000000 wlan.6.prism wlan.props --property cost_min -const COL=0
Parsing model file "wlan.6.prism"...
Type: MDP
Modules: medium station1 station2
Variables: col c1 c2 x1 s1 slot1 backoff1 bc1 x2 s2 slot2 backoff2 bc2
Parsing properties file "wlan.props"...
7 properties:
(1) "collisions": Pmax=? [ F col=COL ]
(2) "cost_max": R{"cost"}max=? [ F s1=12&s2=12 ]
(3) "cost_min": R{"cost"}min=? [ F s1=12&s2=12 ]
(4) "num_collisions": R{"collisions"}max=? [ F s1=12&s2=12 ]
(5) "sent": P>=1 [ F s1=12&s2=12 ]
(6) "time_max": R{"time"}max=? [ F s1=12&s2=12 ]
(7) "time_min": R{"time"}min=? [ F s1=12&s2=12 ]
---------------------------------------------------------------------
Model checking: "cost_min": R{"cost"}min=? [ F s1=12&s2=12 ]
Model constants: COL=0
Warning: Switching to sparse engine and (backwards) Gauss Seidel (default for heuristic=speed).
Warning: Switching to explicit engine to allow interval iteration on Rmin operator.
Building model...
Model constants: COL=0
Computing reachable states... 207102 460461 685865 947326 1311725 1616840 1696698 1860179 2125170 2338085 2567902 2635720 3038495 3434945 3805975 4167754 4579475 4912271 5007548 states
Reachable states exploration and model construction done in 55.436 secs.
Sorting reachable states list...
Time for model construction: 61.318 seconds.
Type: MDP
States: 5007548 (1 initial)
Transitions: 11475748
Choices: 6350470
Max/avg: 3/1.27
Building reward structure...
Starting expected reachability (min)...
Starting Prob1 (max)...
Prob1 (max) took 3101 iterations and 578.444 seconds.
target=1, inf=0, rest=5007547
For Rmin, checking for zero-reward ECs...
Time for checking for zero-reward ECs: 1.675 seconds, no zero-reward ECs found, proceeding normally.
Computing upper bound(s) for Rmin using the Dijkstra Sweep for Monotone Pessimistic Initialization algorithm...
Calculating incoming choices relation for Markov decision process... done (0.864 seconds)
Time for computing upper bound(s) for Rmin using the DSI-MP algorithm: 23.296 seconds.
Upper bound for min expectation (Dijkstra Sweep MPI): 441670.8165168762
Starting Prob1 (min)...
Prob1 (min) took 3158 iterations and 538.386 seconds.
Relevant sub-MDP is contracting, proceed...
Starting interval iteration (min, with Power method)...
Iteration 9: max relative diff=4700.36087436, 5.46 sec so far
Iteration 18: max relative diff=1765.68326607, 10.80 sec so far
Iteration 27: max relative diff=1103.17704129, 16.14 sec so far
Iteration 36: max relative diff=802.037848213, 21.46 sec so far
Iteration 45: max relative diff=629.95830931, 26.78 sec so far
Iteration 54: max relative diff=518.612725314, 32.15 sec so far
Iteration 63: max relative diff=440.670816517, 37.46 sec so far
Iteration 72: max relative diff=383.06157958, 42.78 sec so far
Iteration 81: max relative diff=338.746781936, 48.12 sec so far
Iteration 90: max relative diff=303.600563115, 53.54 sec so far
Iteration 99: max relative diff=275.044260323, 58.87 sec so far
Iteration 108: max relative diff=251.383323724, 64.18 sec so far
Iteration 117: max relative diff=231.458324483, 69.49 sec so far
Iteration 126: max relative diff=214.449178789, 74.83 sec so far
Iteration 135: max relative diff=199.759462053, 80.15 sec so far
Iteration 144: max relative diff=186.945028305, 85.46 sec so far
Iteration 153: max relative diff=175.668326607, 90.78 sec so far
Iteration 162: max relative diff=165.668232648, 96.09 sec so far
Iteration 171: max relative diff=156.739577327, 101.40 sec so far
Iteration 180: max relative diff=148.718920853, 106.75 sec so far
Iteration 189: max relative diff=141.474456941, 112.06 sec so far
Iteration 198: max relative diff=134.898712774, 117.47 sec so far
Iteration 207: max relative diff=128.903181328, 122.80 sec so far
Iteration 216: max relative diff=123.414314512, 128.15 sec so far
Iteration 225: max relative diff=118.370490951, 133.46 sec so far
Iteration 234: max relative diff=113.719692602, 138.82 sec so far
Iteration 243: max relative diff=109.417704129, 144.13 sec so far
Iteration 252: max relative diff=105.426702775, 149.45 sec so far
Iteration 261: max relative diff=101.714143376, 154.77 sec so far
Iteration 270: max relative diff=98.2518688802, 160.09 sec so far
Iteration 279: max relative diff=95.015394895, 165.44 sec so far
Iteration 288: max relative diff=91.983329793, 170.75 sec so far
Iteration 297: max relative diff=89.13690133, 176.07 sec so far
Iteration 306: max relative diff=86.4595676271, 181.41 sec so far
Iteration 315: max relative diff=83.936695484, 186.95 sec so far
Iteration 324: max relative diff=81.5552928069, 192.28 sec so far
Iteration 333: max relative diff=79.3037848213, 197.64 sec so far
Iteration 342: max relative diff=77.1718259322, 202.98 sec so far
Iteration 351: max relative diff=75.1501407788, 208.29 sec so far
Iteration 360: max relative diff=73.2303893306, 213.60 sec so far
Iteration 369: max relative diff=71.405051888, 218.91 sec so far
Iteration 378: max relative diff=69.6673306427, 224.29 sec so far
Iteration 387: max relative diff=68.0110650808, 229.60 sec so far
Iteration 396: max relative diff=66.4306590102, 234.91 sec so far
Iteration 405: max relative diff=64.9210173906, 240.25 sec so far
Iteration 414: max relative diff=63.4774914623, 245.60 sec so far
Iteration 423: max relative diff=62.095830931, 250.92 sec so far
Iteration 432: max relative diff=60.7721421702, 256.47 sec so far
Iteration 441: max relative diff=59.5028515777, 261.80 sec so far
Iteration 450: max relative diff=58.284673358, 267.14 sec so far
Iteration 459: max relative diff=57.1145811206, 272.46 sec so far
Iteration 468: max relative diff=55.9897827764, 277.83 sec so far
Iteration 477: max relative diff=54.9076982933, 283.14 sec so far
Iteration 486: max relative diff=53.86593994, 288.50 sec so far
Iteration 495: max relative diff=52.8622946972, 293.81 sec so far
Iteration 504: max relative diff=51.8947085649, 299.13 sec so far
Iteration 513: max relative diff=50.9612725314, 304.44 sec so far
Iteration 522: max relative diff=50.060210002, 309.77 sec so far
Iteration 531: max relative diff=49.1898655133, 315.10 sec so far
Iteration 540: max relative diff=48.3486945829, 320.42 sec so far
Iteration 549: max relative diff=47.5352545623, 325.96 sec so far
Iteration 558: max relative diff=46.7481963802, 331.31 sec so far
Iteration 567: max relative diff=45.9862570763, 336.62 sec so far
Iteration 576: max relative diff=45.2482530384, 341.94 sec so far
Iteration 585: max relative diff=44.5330738677, 347.27 sec so far
Iteration 594: max relative diff=43.8396768037, 352.60 sec so far
Iteration 603: max relative diff=43.1670816517, 357.91 sec so far
Iteration 612: max relative diff=42.5143661593, 363.22 sec so far
Iteration 621: max relative diff=41.8806617978, 368.54 sec so far
Iteration 630: max relative diff=41.2651499059, 373.87 sec so far
Iteration 639: max relative diff=40.667058162, 379.19 sec so far
Iteration 648: max relative diff=40.0856573504, 384.50 sec so far
Iteration 657: max relative diff=39.520258396, 389.82 sec so far
Iteration 666: max relative diff=38.9702096395, 395.27 sec so far
Iteration 675: max relative diff=38.4348943319, 400.63 sec so far
Iteration 684: max relative diff=37.9137283275, 405.95 sec so far
Iteration 693: max relative diff=37.406157958, 411.26 sec so far
Iteration 702: max relative diff=36.9116580701, 416.59 sec so far
Iteration 711: max relative diff=36.4297302133, 421.90 sec so far
Iteration 720: max relative diff=35.9599009638, 427.21 sec so far
Iteration 729: max relative diff=35.5017203733, 432.52 sec so far
Iteration 738: max relative diff=35.054760532, 437.86 sec so far
Iteration 747: max relative diff=34.6186142352, 443.16 sec so far
Iteration 756: max relative diff=34.1928937464, 448.47 sec so far
Iteration 765: max relative diff=33.777229647, 453.78 sec so far
Iteration 774: max relative diff=33.3712697679, 459.26 sec so far
Iteration 783: max relative diff=32.9746781936, 464.60 sec so far
Iteration 792: max relative diff=32.5871343359, 469.92 sec so far
Iteration 801: max relative diff=32.2083320689, 475.25 sec so far
Iteration 810: max relative diff=31.8379789232, 480.60 sec so far
Iteration 819: max relative diff=31.4757953321, 485.91 sec so far
Iteration 828: max relative diff=31.1215139285, 491.21 sec so far
Iteration 837: max relative diff=30.7748788861, 496.54 sec so far
Iteration 846: max relative diff=30.4356453037, 501.86 sec so far
Iteration 855: max relative diff=30.1035786279, 507.19 sec so far
Iteration 864: max relative diff=29.7784541127, 512.50 sec so far
Iteration 873: max relative diff=29.4600563115, 517.80 sec so far
Iteration 882: max relative diff=29.1481786018, 523.14 sec so far
Iteration 889: max relative diff=28.9437841706, 528.21 sec so far
Iteration 898: max relative diff=28.642336679, 533.53 sec so far
Iteration 907: max relative diff=28.3468981074, 538.84 sec so far
Iteration 916: max relative diff=28.0572905603, 544.16 sec so far
Iteration 925: max relative diff=27.7733430956, 549.49 sec so far
Iteration 934: max relative diff=27.4948913882, 554.81 sec so far
Iteration 943: max relative diff=27.2217774132, 560.10 sec so far
Iteration 952: max relative diff=26.9538491466, 565.41 sec so far
Iteration 961: max relative diff=26.6909602832, 570.72 sec so far
Iteration 970: max relative diff=26.43296997, 576.02 sec so far
Iteration 979: max relative diff=26.1797425549, 581.31 sec so far
Iteration 988: max relative diff=25.9311473486, 586.62 sec so far
Iteration 997: max relative diff=25.6870583998, 591.94 sec so far
----------
Computation aborted after 1800.3046743869781 seconds since the total time limit of 1800 seconds was exceeded.